Nuprl Lemma : multiply_functionality_wrt_le 13,42

i1i2j1j2:. (i1  j1 (i2  j2 ((i1 * i2 (j1 * j2)) 
latex


Upint 2, int 2
Definitionst  T, P  Q, x:AB(x), False, A, A  B, ,
Lemmasnat wf, le wf, mul preserves le

origin